Predikaatloogika ehk predikaatarvutus on lauseloogika laienduste klass, kus lisaks lausesümbolitele ja konnektoritele on kasutusel vähemalt predikaadisümbolid, indiviidikonstandid, muutujad (indiviidimuutujad) ja kvantorid. Mõnikord nimetatakse predikaatarvutuseks aksiomatiseeritud predikaatloogikat.
Predikaatloogika kasutab kvantifitseeritud muutujaid mitteloogiliste objektide asemel ning lubab kasutada lauseid, mis sisaldavad muutujaid. See tähendab, et selle asemel et kirjutada väide "Sokrates on inimene" võib avaldisi kirjutada vormis "eksisteerib x nõnda, et x on Sokrates ja x on inimene," kus "eksisteerib" on kvantor ning x on muutuja.[1] See eristab seda lauseloogikast, mis ei kasuta muutujaid ega seoseid.[2] Selles mõttes on lauseloogika predikaatloogika alus.
Teooria mingi teema kohta, näiteks hulgateooria, teooria gruppide kohta[3] või formaalne teooria aritmeetika kohta rajatakse tavaliselt predikaatloogikale koos antud teooriaga seotud diskursuse domeeniga (universaalse hulgaga, üle mille kvantifitseeritud muutujad ulatuvad) koos piiratud arvu funktsioonidega sellest domeenist iseendasse, piiratud arvu predikaatidega, mis sellel domeenil on defineeritud; ning hulga aksioomidega, mille paikapidavust nende kohta usutakse.
Lihtsaim ja levinuim predikaatloogika süsteem on esimese järgu loogika, mida sageli nimetataksegi lihtsalt predikaatloogikaks. See eristab seda kõrgema järgu loogikast, milles võivad predikaadid või funktsioonid olla predikaatide argumendid, või milles on lubatud kvantifikatsioon üle predikaatide, funktsioonide või mõlema.[4][5] Esimese järgu teooriates on predikaadid sageli seotud hulkadega. Interpreteeritud kõrgema järgu teooriates võivad predikaadid olla interpreteeritud kui hulkadest koosnevad hulgad.